Inference at * 1 2 
Iof proof for Lemma mul cancel in eq:



1. a : 
2. b : 
3. n : 
4. m:. ((m * a) = (m * b))  (a = b)
5. (n * a) = (n * b)
  a = b 

latex

 by ((Decide n > 0) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 6. n > 0
C1:   a = b
C2: 

C2: 6. (n > 0)
C2:   a = b
C.

Definitions	t  T, i > j, P  Q, Dec(P), x:A. B(x),
Lemmas	decidable lt